1. Technical Field
The present invention relates to computer verification and more particularly to systems and methods for analyzing programs statically using abstract interpretation for a path-sensitive analysis using a path-insensitive analysis.
2. Description of the Related Art
There have been three significant categories that incorporate path sensitivity into program analysis: (a) performing a path-sensitive analysis, selectively merging or separating the contributions from different program points in the analysis; (b) performing a disjunctive completion of the abstract domain to track disjunctive invariants directly. However, the process is expensive and not entirely practical; (c) performing repeated abstraction refinements, either by changing the iteration scheme used to effectively unroll loops further or using a fixpoint-guided abstraction-refinement scheme).
Static analysis techniques compute sound over-approximations of the set of reachable states of a given program. Such an over-approximation is computed as a fixpoint in a suitably chosen abstract domain using abstract interpretation. Abstract interpretation controls the precision of the analysis through a judicious choice of an abstract domain.
The static analyzer may report false positives due to the over-approximations. The precision lost due to the over-approximations may be recovered in part through techniques such as path sensitive analysis, disjunctive completion and domain refinement, as described above. Path-sensitive analyses reason about different sets of program paths in isolation, thus minimizing the impact of the join operation at the merge points in the program. However, a completely path-sensitive analysis is forbiddingly expensive in practice. Therefore, many static-analysis algorithms aim for intermediate solutions that selectively join or separate the contributions due to different paths to achieve a degree of path sensitivity that is adequate to prove properties at hand. Such approaches rely on heuristics to determine whether to merge contributions from different paths in the analysis, or alternatively, keep them as separate disjuncts.
Recent work on abstract interpretation has been focused on refining the initial abstract domain or the iteration itself to obtain incrementally more precise results. In practice, we found that many syntactic paths in a control flow graph (CFG) representation of the program are semantically infeasible, i.e., they may not be traversed by any execution of the program. Reasoning about the infeasibility of such paths is a key factor in performing accurate static analyses for checking properties such as correct application program interface (API) usage, absence of null-pointer dereferences and uninitialized use of variables, memory leaks, and so on.